Nuprl Lemma : gcd_unique 11,40

a,b,y1,y2:. gcd_p(aby1 gcd_p(aby2 assoced(y1y2
latex


Definitionsprop{i:l}, t  T, P  Q, assoced(ab), gcd_p(aby), P  Q, x:AB(x)
Lemmasdivides wf

origin